M:MsgA, l:IdLnk, tg:Id. rcv(l,tg) declared in M  (M.din(l,tg) ~ Top) 

latex

Definitions	x:A. B(x), b, t  T, b, Prop, , False, P  Q, A, Knd, rcv(l,tg), x  dom(f), P & Q, P  Q, Unit, f(x)?z, x. t(x), a:A fp B(a), KindDeq, Id, IdLnk, M.din(l,tg), rcv(l,tg) declared in M, MsgA
Lemmas	msga wf, IdLnk wf, Id wf, not wf, Kind-deq wf, rcv wf, fpf-trivial-subtype-top, Knd wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, bool wf, assert wf, bnot wf